($\lambda$$A$,$B$,$p$,$z$. $p$.2) $\in$ $A$:Type$\rightarrow$$B$:($A$$\rightarrow$Type)$\rightarrow$$p$:($a$:$A$ $\times$ $B$($a$))$\rightarrow$($\downarrow$True)$\rightarrow$$B$($p$.1)